/**
 * Provides classes for working with basic blocks, and predicates for computing
 * liveness information for local variables.
 */
overlay[local]
module;

import javascript
private import semmle.javascript.internal.StmtContainers
private import semmle.javascript.internal.CachedStages
private import codeql.controlflow.BasicBlock as BB

/**
 * Holds if `nd` starts a new basic block.
 */
private predicate startsBB(ControlFlowNode nd) {
  not exists(nd.getAPredecessor()) and exists(nd.getASuccessor())
  or
  nd.isJoin()
  or
  nd.getAPredecessor().isBranch()
}

/**
 * Holds if the first node of basic block `succ` is a control flow
 * successor of the last node of basic block `bb`.
 */
private predicate succBB(BasicBlock bb, BasicBlock succ) { succ = bb.getLastNode().getASuccessor() }

/**
 * Holds if the first node of basic block `bb` is a control flow
 * successor of the last node of basic block `pre`.
 */
private predicate predBB(BasicBlock bb, BasicBlock pre) { succBB(pre, bb) }

/** Holds if `bb` is an entry basic block. */
private predicate entryBB(BasicBlock bb) { bb.getFirstNode() instanceof ControlFlowEntryNode }

/** Holds if `bb` is an exit basic block. */
private predicate exitBB(BasicBlock bb) { bb.getLastNode() instanceof ControlFlowExitNode }

cached
private module Cached {
  /**
   * Holds if `succ` is a control flow successor of `nd` within the same basic block.
   */
  private predicate intraBBSucc(ControlFlowNode nd, ControlFlowNode succ) {
    succ = nd.getASuccessor() and
    not succ instanceof BasicBlock
  }

  /**
   * Holds if `nd` is the `i`th node in basic block `bb`.
   *
   * In other words, `i` is the shortest distance from a node `bb`
   * that starts a basic block to `nd` along the `intraBBSucc` relation.
   */
  cached
  predicate bbIndex(BasicBlock bb, ControlFlowNode nd, int i) =
    shortestDistances(startsBB/1, intraBBSucc/2)(bb, nd, i)

  cached
  int bbLength(BasicBlock bb) { result = strictcount(ControlFlowNode nd | bbIndex(bb, nd, _)) }

  cached
  predicate useAt(BasicBlock bb, int i, Variable v, VarUse u) {
    Stages::BasicBlocks::ref() and
    v = u.getVariable() and
    bbIndex(bb, u, i)
  }

  cached
  predicate defAt(BasicBlock bb, int i, Variable v, VarDef d, VarRef lhs) {
    (
      lhs = d.getTarget().(BindingPattern).getABindingVarRef() and
      v = lhs.getVariable()
    ) and
    (
      lhs = d.getTarget() and
      bbIndex(bb, d, i)
      or
      exists(PropertyPattern pp |
        lhs = pp.getValuePattern() and
        bbIndex(bb, pp, i)
      )
      or
      exists(ObjectPattern op |
        lhs = op.getRest() and
        bbIndex(bb, lhs, i)
      )
      or
      exists(ArrayPattern ap |
        lhs = ap.getAnElement() and
        bbIndex(bb, lhs, i)
      )
    )
  }

  cached
  predicate reachableBB(BasicBlock bb) {
    entryBB(bb)
    or
    exists(BasicBlock predBB | succBB(predBB, bb) | reachableBB(predBB))
  }
}

private import Cached

/** Gets the immediate dominator of `bb`. */
cached
BasicBlock immediateDominator(BasicBlock bb) = idominance(entryBB/1, succBB/2)(_, result, bb)

/** Gets the immediate post-dominator of `bb`. */
cached
BasicBlock immediatePostDominator(BasicBlock bb) = idominance(exitBB/1, predBB/2)(_, result, bb)

import Public

module Public {
  /**
   * A basic block, that is, a maximal straight-line sequence of control flow nodes
   * without branches or joins.
   *
   * At the database level, a basic block is represented by its first control flow node.
   */
  class BasicBlock extends @cfg_node, NodeInStmtContainer {
    cached
    BasicBlock() { Stages::BasicBlocks::ref() and startsBB(this) }

    /** Gets a basic block succeeding this one. */
    BasicBlock getASuccessor() { succBB(this, result) }

    /** Gets a basic block preceding this one. */
    BasicBlock getAPredecessor() { result.getASuccessor() = this }

    /** Gets a node in this block. */
    ControlFlowNode getANode() { result = this.getNode(_) }

    /** Gets the node at the given position in this block. */
    ControlFlowNode getNode(int pos) { bbIndex(this, result, pos) }

    /** Gets the first node in this block. */
    ControlFlowNode getFirstNode() { result = this }

    /** Gets the last node in this block. */
    ControlFlowNode getLastNode() { result = this.getNode(this.length() - 1) }

    /** Gets the length of this block. */
    int length() { result = bbLength(this) }

    /** Holds if this basic block uses variable `v` in its `i`th node `u`. */
    predicate useAt(int i, Variable v, VarUse u) { useAt(this, i, v, u) }

    /** Holds if this basic block defines variable `v` in its `i`th node `d`. */
    predicate defAt(int i, Variable v, VarDef d) { defAt(this, i, v, d, _) }

    /** Holds if this basic block defines variable `v` in its `i`th node `d`, and `lhs` is the corresponding variable reference. */
    predicate defAt(int i, Variable v, VarDef d, VarRef lhs) { defAt(this, i, v, d, lhs) }

    /**
     * Holds if `v` is live at entry to this basic block and `u` is a use of `v`
     * witnessing the liveness.
     *
     * In other words, `u` is a use of `v` that is reachable from the
     * entry node of this basic block without going through a redefinition
     * of `v`. The use `u` may either be in this basic block, or in another
     * basic block reachable from this one.
     */
    predicate isLiveAtEntry(Variable v, VarUse u) {
      // restrict `u` to be reachable from this basic block
      u = this.getASuccessor*().getANode() and
      (
        // shortcut: if `v` is never defined, then it must be live
        this.isDefinedInSameContainer(v)
        implies
        // otherwise, do full liveness computation
        this.isLiveAtEntryImpl(v, u)
      )
    }

    /**
     * Holds if `v` is live at entry to this basic block and `u` is a use of `v`
     * witnessing the liveness, where `v` is defined at least once in the enclosing
     * function or script.
     */
    private predicate isLiveAtEntryImpl(Variable v, VarUse u) {
      this.isLocallyLiveAtEntry(v, u)
      or
      this.isDefinedInSameContainer(v) and
      not this.defAt(_, v, _) and
      this.getASuccessor().isLiveAtEntryImpl(v, u)
    }

    /**
     * Holds if `v` is defined at least once in the function or script to which
     * this basic block belongs.
     */
    private predicate isDefinedInSameContainer(Variable v) {
      exists(VarDef def | def.getAVariable() = v and def.getContainer() = this.getContainer())
    }

    /**
     * Holds if `v` is a variable that is live at entry to this basic block.
     *
     * Note that this is equivalent to `bb.isLiveAtEntry(v, _)`, but may
     * be more efficient on large databases.
     */
    predicate isLiveAtEntry(Variable v) {
      this.isLocallyLiveAtEntry(v, _)
      or
      not this.defAt(_, v, _) and this.getASuccessor().isLiveAtEntry(v)
    }

    /**
     * Holds if local variable `v` is live at entry to this basic block and
     * `u` is a use of `v` witnessing the liveness.
     */
    predicate localIsLiveAtEntry(LocalVariable v, VarUse u) {
      this.isLocallyLiveAtEntry(v, u)
      or
      not this.defAt(_, v, _) and this.getASuccessor().localIsLiveAtEntry(v, u)
    }

    /**
     * Holds if local variable `v` is live at entry to this basic block.
     */
    predicate localIsLiveAtEntry(LocalVariable v) {
      this.isLocallyLiveAtEntry(v, _)
      or
      not this.defAt(_, v, _) and this.getASuccessor().localIsLiveAtEntry(v)
    }

    /**
     * Holds if `d` is a definition of `v` that is reachable from the beginning of
     * this basic block without going through a redefinition of `v`.
     */
    predicate localMayBeOverwritten(LocalVariable v, VarDef d) {
      this.isLocallyOverwritten(v, d)
      or
      not this.defAt(_, v, _) and this.getASuccessor().localMayBeOverwritten(v, d)
    }

    /**
     * Gets the next index after `i` in this basic block at which `v` is
     * defined or used, provided that `d` is a definition of `v` at index `i`.
     * If there are no further uses or definitions of `v` after `i`, the
     * result is the length of this basic block.
     */
    private int nextDefOrUseAfter(PurelyLocalVariable v, int i, VarDef d) {
      this.defAt(i, v, d) and
      result =
        min(int j |
          (this.defAt(j, v, _) or this.useAt(j, v, _) or j = this.length()) and
          j > i
        )
    }

    /**
     * Holds if `d` defines variable `v` at the `i`th node of this basic block, and
     * the definition is live, that is, the variable may be read after this
     * definition and before a re-definition.
     */
    predicate localLiveDefAt(PurelyLocalVariable v, int i, VarDef d) {
      exists(int j | j = this.nextDefOrUseAfter(v, i, d) |
        this.useAt(j, v, _)
        or
        j = this.length() and this.getASuccessor().localIsLiveAtEntry(v)
      )
    }

    /**
     * Holds if `u` is a use of `v` in this basic block, and there are
     * no definitions of `v` before it.
     */
    private predicate isLocallyLiveAtEntry(Variable v, VarUse u) {
      exists(int n | this.useAt(n, v, u) | not exists(int m | m < n | this.defAt(m, v, _)))
    }

    /**
     * Holds if `d` is a definition of `v` in this basic block, and there are
     * no other definitions of `v` before it.
     */
    private predicate isLocallyOverwritten(Variable v, VarDef d) {
      exists(int n | this.defAt(n, v, d) | not exists(int m | m < n | this.defAt(m, v, _)))
    }

    /**
     * Gets the basic block that immediately dominates this basic block.
     */
    ReachableBasicBlock getImmediateDominator() { result = immediateDominator(this) }

    /**
     * Holds if this if a basic block whose last node is an exit node.
     */
    predicate isExitBlock() { exitBB(this) }
  }

  /**
   * An unreachable basic block, that is, a basic block
   * whose first node is unreachable.
   */
  class UnreachableBlock extends BasicBlock {
    UnreachableBlock() { this.getFirstNode().isUnreachable() }
  }

  /**
   * An entry basic block, that is, a basic block
   * whose first node is the entry node of a statement container.
   */
  class EntryBasicBlock extends BasicBlock {
    EntryBasicBlock() { entryBB(this) }
  }

  /**
   * A basic block that is reachable from an entry basic block.
   */
  class ReachableBasicBlock extends BasicBlock {
    ReachableBasicBlock() { reachableBB(this) }

    /**
     * Holds if this basic block strictly dominates `bb`.
     */
    overlay[caller]
    pragma[inline]
    predicate strictlyDominates(ReachableBasicBlock bb) { this = immediateDominator+(bb) }

    /**
     * Holds if this basic block dominates `bb`.
     *
     * This predicate is reflexive: each reachable basic block dominates itself.
     */
    overlay[caller]
    pragma[inline]
    predicate dominates(ReachableBasicBlock bb) { this = immediateDominator*(bb) }

    /**
     * Holds if this basic block strictly post-dominates `bb`.
     */
    overlay[caller]
    pragma[inline]
    predicate strictlyPostDominates(ReachableBasicBlock bb) { this = immediatePostDominator+(bb) }

    /**
     * Holds if this basic block post-dominates `bb`.
     *
     * This predicate is reflexive: each reachable basic block post-dominates itself.
     */
    overlay[caller]
    pragma[inline]
    predicate postDominates(ReachableBasicBlock bb) { this = immediatePostDominator*(bb) }
  }

  /**
   * A reachable basic block with more than one predecessor.
   */
  class ReachableJoinBlock extends ReachableBasicBlock {
    ReachableJoinBlock() { this.getFirstNode().isJoin() }

    /**
     * Holds if this basic block belongs to the dominance frontier of `b`, that is
     * `b` dominates a predecessor of this block, but not this block itself.
     *
     * Algorithm from Cooper et al., "A Simple, Fast Dominance Algorithm" (Figure 5),
     * who in turn attribute it to Ferrante et al., "The program dependence graph and
     * its use in optimization".
     */
    predicate inDominanceFrontierOf(ReachableBasicBlock b) {
      b = this.getAPredecessor() and not b = this.getImmediateDominator()
      or
      exists(ReachableBasicBlock prev | this.inDominanceFrontierOf(prev) |
        b = prev.getImmediateDominator() and
        not b = this.getImmediateDominator()
      )
    }
  }

  final private class FinalBasicBlock = BasicBlock;

  module Cfg implements BB::CfgSig<Location> {
    private import javascript as Js
    private import codeql.controlflow.SuccessorType

    class ControlFlowNode = Js::ControlFlowNode;

    private predicate conditionSucc(BasicBlock bb1, BasicBlock bb2, boolean branch) {
      exists(ConditionGuardNode g |
        bb1 = g.getTest().getBasicBlock() and
        bb2 = g.getBasicBlock() and
        branch = g.getOutcome()
      )
    }

    class BasicBlock extends FinalBasicBlock {
      BasicBlock getASuccessor() { result = super.getASuccessor() }

      BasicBlock getASuccessor(SuccessorType t) {
        conditionSucc(this, result, t.(BooleanSuccessor).getValue())
        or
        result = super.getASuccessor() and
        t instanceof DirectSuccessor and
        not conditionSucc(this, result, _)
      }

      predicate strictlyDominates(BasicBlock bb) {
        this.(ReachableBasicBlock).strictlyDominates(bb)
      }

      predicate dominates(BasicBlock bb) { this.(ReachableBasicBlock).dominates(bb) }

      predicate inDominanceFrontier(BasicBlock df) {
        df.(ReachableJoinBlock).inDominanceFrontierOf(this)
      }

      BasicBlock getImmediateDominator() { result = super.getImmediateDominator() }

      predicate strictlyPostDominates(BasicBlock bb) {
        this.(ReachableBasicBlock).strictlyPostDominates(bb)
      }

      predicate postDominates(BasicBlock bb) { this.(ReachableBasicBlock).postDominates(bb) }
    }

    class EntryBasicBlock extends BasicBlock {
      EntryBasicBlock() { entryBB(this) }
    }

    pragma[nomagic]
    predicate dominatingEdge(BasicBlock bb1, BasicBlock bb2) {
      bb1.getASuccessor() = bb2 and
      bb1 = bb2.getImmediateDominator() and
      forall(BasicBlock pred | pred = bb2.getAPredecessor() and pred != bb1 | bb2.dominates(pred))
    }
  }
}
